End-users of certain microprocessor-based products rely on the hardware system to function correctly all the time and for every task. To meet this expectation, microprocessor design houses perform extensive validation of their designs before production and release to the marketplace. The success of this process may be important to the survival of the company, as the financial impact of microprocessor bugs can be devastating.
Designers address correctness concerns through verification, the process of extensively validating all the functionalities of a design throughout the development cycle. Simulation-based techniques are central to this process: they exercise a design with relevant test sequences in the attempt to expose latent bugs. This approach is used extensively in the industry, yet it suffers from a number of drawbacks. First, simulation-based verification is a non-exhaustive process: the density of states in modern microprocessors is too large to allow for the entire state space to be fully exercised. For example, a simple out-of-order processor core may have 128 inputs signals, 31 64-bit registers and additional control states for a total of 210441 distinct configurations, each with up to 2128 outgoing edges connecting to other configurations. In contrast, the verification of the Pentium 4, which utilized a simulation pool of 6,000 workstations, was only able to test 2 states prior to tape-out.
Formal verification techniques have grown to address the non-exhaustive nature of simulation-based methods. Formal methods (such as theorem provers and model checkers) enable an engineer to reason about the correctness of a hardware component, regardless of the programs and storage state impressed upon the design. In some scenarios, it is possible to prove that a design will not exhibit a certain failure property, or that it will never produce a result that differs from a known-correct reference model. The primary drawback of formal techniques, however, is that they do not scale to the complexity of modern designs, limiting their deployment and benefit to only a few components within the overall design. For example, the verification of the Pentium 4 heavily utilized formal verification tools, but their use was limited to proving properties of the floating-point units, the instruction decoders and the dynamic scheduler.
Unfortunately, the situation seems to be deteriorating in the presence of seemingly unending design complexity scaling, which is in contrast with the much slower growth of the capabilities of verification tools, leading to what is referred to as the “verification gap.” In the end, processor designs are released not fully tested, and hence, with latent bugs.